\begin{tabbing}
$\forall$\=${\it es}$:ES, $A$:Type, $i$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type,\+
\\[0ex]${\it conds}$:$k$:Knd fp$\rightarrow$ $V$:Type $\times$ (State(${\it ds}$)$\rightarrow$$V$$\rightarrow$($A$ + Top)).
\-\\[0ex]($\forall$$e$:E.
\\[0ex](loc($e$) = $i$)
\\[0ex]$\Rightarrow$ ($\uparrow$kind($e$) $\in$ dom(${\it conds}$))
\\[0ex]$\Rightarrow$ ((valtype($e$) $\subseteq$r (${\it conds}$(kind($e$)).1)) \& (state@loc($e$) $\subseteq$r State(${\it ds}$))))
\\[0ex]$\Rightarrow$ \=($\forall$$e$:E.\+
\\[0ex]($\uparrow$($e$ $\in_{b}$ es{-}triggers(${\it es}$;$i$;${\it ds}$;${\it conds}$)))
\\[0ex]$\Leftarrow\!\Rightarrow$ \=(loc($e$) = $i$ \& (kind($e$) $\in$ fpf{-}domain(${\it conds}$))\+
\\[0ex]\& ($\uparrow$isl((${\it conds}$(kind($e$)).2)((state when $e$),val($e$))))))
\-\-
\end{tabbing}